the_es:ES, l:IdLnk, e':E, m:(Msg on l).
(m  msgs(l;before(e')))  (e:E. (e <loc e') & haslnk(l;e) & m = emsg(e)) 

latex

Definitions	SqStable(P), T, True, l[i], S  T, , AB, A, False, ||as||, msgs(l;before(e')), x. t(x), map(f;as), rcvs(l;before(e')), haslnk(l;e), emsg(e), ES, IdLnk, x:A. B(x), P  Q, P  Q, P  Q, A & B, (e <loc e'), t  T, Prop, x:A. B(x), P & Q, (Msg on l), (x  l), b, E
Lemmas	es-msg wf2, l member wf, es-haslnk wf, assert wf, es-locl wf, es-rcvs wf, map wf, es-Msgl wf, es-E wf, IdLnk wf, event system wf, member map, iff functionality wrt iff, all functionality wrt iff, select wf, length wf1, member-es-rcvs, decidable assert, sq stable from decidable